Runtime Complexity (innermost) proof of /tmp/tmprt5GoB/clevermmult.raml.xml

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2).

0 CpxRelTRS

↳1 RelTrsToTrsProof (UPPER BOUND(ID), 0 ms)

↳2 CpxTRS

↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CdtProblem

↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳8 CdtProblem

↳9 CdtUsableRulesProof (⇔, 31 ms)

↳10 CdtProblem

↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 333 ms)

↳12 CdtProblem

↳13 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 233 ms)

↳16 CdtProblem

↳17 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 1008 ms)

↳20 CdtProblem

↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 800 ms)

↳22 CdtProblem

↳23 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 504 ms)

↳24 CdtProblem

↳25 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳26 CdtProblem

↳27 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 493 ms)

↳28 CdtProblem

↳29 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 395 ms)

↳30 CdtProblem

↳31 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)

↳32 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

*(@x, @y) → #mult(@x, @y)
+(@x, @y) → #add(@x, @y)
computeLine(@line, @m, @acc) → computeLine#1(@line, @acc, @m)
computeLine#1(::(@x, @xs), @acc, @m) → computeLine#2(@m, @acc, @x, @xs)
computeLine#1(nil, @acc, @m) → @acc
computeLine#2(::(@l, @ls), @acc, @x, @xs) → computeLine(@xs, @ls, lineMult(@x, @l, @acc))
computeLine#2(nil, @acc, @x, @xs) → nil
lineMult(@n, @l1, @l2) → lineMult#1(@l1, @l2, @n)
lineMult#1(::(@x, @xs), @l2, @n) → lineMult#2(@l2, @n, @x, @xs)
lineMult#1(nil, @l2, @n) → nil
lineMult#2(::(@y, @ys), @n, @x, @xs) → ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
lineMult#2(nil, @n, @x, @xs) → ::(*(@x, @n), lineMult(@n, @xs, nil))
matrixMult(@m1, @m2) → matrixMult#1(@m1, @m2)
matrixMult#1(::(@l, @ls), @m2) → ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2))
matrixMult#1(nil, @m2) → nil

The (relative) TRS S consists of the following rules:

#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Rewrite Strategy: INNERMOST

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

transformed relative TRS to TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

*(@x, @y) → #mult(@x, @y)
+(@x, @y) → #add(@x, @y)
computeLine(@line, @m, @acc) → computeLine#1(@line, @acc, @m)
computeLine#1(::(@x, @xs), @acc, @m) → computeLine#2(@m, @acc, @x, @xs)
computeLine#1(nil, @acc, @m) → @acc
computeLine#2(::(@l, @ls), @acc, @x, @xs) → computeLine(@xs, @ls, lineMult(@x, @l, @acc))
computeLine#2(nil, @acc, @x, @xs) → nil
lineMult(@n, @l1, @l2) → lineMult#1(@l1, @l2, @n)
lineMult#1(::(@x, @xs), @l2, @n) → lineMult#2(@l2, @n, @x, @xs)
lineMult#1(nil, @l2, @n) → nil
lineMult#2(::(@y, @ys), @n, @x, @xs) → ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
lineMult#2(nil, @n, @x, @xs) → ::(*(@x, @n), lineMult(@n, @xs, nil))
matrixMult(@m1, @m2) → matrixMult#1(@m1, @m2)
matrixMult#1(::(@l, @ls), @m2) → ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2))
matrixMult#1(nil, @m2) → nil
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Rewrite Strategy: INNERMOST

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

*(z0, z1) → #mult(z0, z1)
+(z0, z1) → #add(z0, z1)
computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1)
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1)
computeLine#1(nil, z0, z1) → z0
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2))
computeLine#2(nil, z0, z1, z2) → nil
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
matrixMult(z0, z1) → matrixMult#1(z0, z1)
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2))
matrixMult#1(nil, z0) → nil
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#1(nil, z0, z1) → c4
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
COMPUTELINE#2(nil, z0, z1, z2) → c6
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#1(nil, z0, z1) → c9
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
MATRIXMULT#1(nil, z0) → c14
#ADD(#0, z0) → c15
#ADD(#neg(#s(#0)), z0) → c16(#PRED(z0))
#ADD(#neg(#s(#s(z0))), z1) → c17(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#0)), z0) → c18(#SUCC(z0))
#ADD(#pos(#s(#s(z0))), z1) → c19(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#MULT(#0, #0) → c20
#MULT(#0, #neg(z0)) → c21
#MULT(#0, #pos(z0)) → c22
#MULT(#neg(z0), #0) → c23
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #0) → c26
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#0, z0) → c29
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#PRED(#0) → c31
#PRED(#neg(#s(z0))) → c32
#PRED(#pos(#s(#0))) → c33
#PRED(#pos(#s(#s(z0)))) → c34
#SUCC(#0) → c35
#SUCC(#neg(#s(#0))) → c36
#SUCC(#neg(#s(#s(z0)))) → c37
#SUCC(#pos(#s(z0))) → c38

S tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#1(nil, z0, z1) → c4
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
COMPUTELINE#2(nil, z0, z1, z2) → c6
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#1(nil, z0, z1) → c9
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
MATRIXMULT#1(nil, z0) → c14
#ADD(#0, z0) → c15
#ADD(#neg(#s(#0)), z0) → c16(#PRED(z0))
#ADD(#neg(#s(#s(z0))), z1) → c17(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#0)), z0) → c18(#SUCC(z0))
#ADD(#pos(#s(#s(z0))), z1) → c19(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#MULT(#0, #0) → c20
#MULT(#0, #neg(z0)) → c21
#MULT(#0, #pos(z0)) → c22
#MULT(#neg(z0), #0) → c23
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #0) → c26
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#0, z0) → c29
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#PRED(#0) → c31
#PRED(#neg(#s(z0))) → c32
#PRED(#pos(#s(#0))) → c33
#PRED(#pos(#s(#s(z0)))) → c34
#SUCC(#0) → c35
#SUCC(#neg(#s(#0))) → c36
#SUCC(#neg(#s(#s(z0)))) → c37
#SUCC(#pos(#s(z0))) → c38

K tuples:none
Defined Rule Symbols:

*, +, computeLine, computeLine#1, computeLine#2, lineMult, lineMult#1, lineMult#2, matrixMult, matrixMult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #ADD, #MULT, #NATMULT, #PRED, #SUCC

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 21 trailing nodes:

#MULT(#0, #neg(z0)) → c21
#SUCC(#0) → c35
#PRED(#0) → c31
#MULT(#0, #0) → c20
#SUCC(#neg(#s(#0))) → c36
#PRED(#pos(#s(#s(z0)))) → c34
#MULT(#neg(z0), #0) → c23
COMPUTELINE#1(nil, z0, z1) → c4
#MULT(#pos(z0), #0) → c26
COMPUTELINE#2(nil, z0, z1, z2) → c6
#ADD(#0, z0) → c15
#SUCC(#pos(#s(z0))) → c38
#PRED(#neg(#s(z0))) → c32
MATRIXMULT#1(nil, z0) → c14
#MULT(#0, #pos(z0)) → c22
#PRED(#pos(#s(#0))) → c33
#NATMULT(#0, z0) → c29
LINEMULT#1(nil, z0, z1) → c9
#ADD(#neg(#s(#0)), z0) → c16(#PRED(z0))
#SUCC(#neg(#s(#s(z0)))) → c37
#ADD(#pos(#s(#0)), z0) → c18(#SUCC(z0))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

*(z0, z1) → #mult(z0, z1)
+(z0, z1) → #add(z0, z1)
computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1)
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1)
computeLine#1(nil, z0, z1) → z0
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2))
computeLine#2(nil, z0, z1, z2) → nil
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
matrixMult(z0, z1) → matrixMult#1(z0, z1)
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2))
matrixMult#1(nil, z0) → nil
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#ADD(#neg(#s(#s(z0))), z1) → c17(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))

S tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#ADD(#neg(#s(#s(z0))), z1) → c17(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))

K tuples:none
Defined Rule Symbols:

*, +, computeLine, computeLine#1, computeLine#2, lineMult, lineMult#1, lineMult#2, matrixMult, matrixMult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #ADD, #MULT, #NATMULT

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c17, c19, c24, c25, c27, c28, c30

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

*(z0, z1) → #mult(z0, z1)
+(z0, z1) → #add(z0, z1)
computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1)
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1)
computeLine#1(nil, z0, z1) → z0
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2))
computeLine#2(nil, z0, z1, z2) → nil
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
matrixMult(z0, z1) → matrixMult#1(z0, z1)
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2))
matrixMult#1(nil, z0) → nil
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

K tuples:none
Defined Rule Symbols:

*, +, computeLine, computeLine#1, computeLine#2, lineMult, lineMult#1, lineMult#2, matrixMult, matrixMult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(9) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1)
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1)
computeLine#1(nil, z0, z1) → z0
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2))
computeLine#2(nil, z0, z1, z2) → nil
matrixMult(z0, z1) → matrixMult#1(z0, z1)
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2))
matrixMult#1(nil, z0) → nil

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
+(z0, z1) → #add(z0, z1)
*(z0, z1) → #mult(z0, z1)
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

K tuples:none
Defined Rule Symbols:

lineMult, lineMult#1, lineMult#2, +, *, #mult, #natmult, #add, #succ, #pred

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))

We considered the (Usable) Rules:

#succ(#0) → #pos(#s(#0))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#succ(#neg(#s(#0))) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#mult(#0, #neg(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#0, #0) → #0
*(z0, z1) → #mult(z0, z1)
#natmult(#0, z0) → #0
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))

And the Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(#0) = 0
POL(#ADD(x₁, x₂)) = x₁
POL(#MULT(x₁, x₂)) = 0
POL(#NATMULT(x₁, x₂)) = 0
POL(#add(x₁, x₂)) = x₁ + x₂
POL(#mult(x₁, x₂)) = 0
POL(#natmult(x₁, x₂)) = 0
POL(#neg(x₁)) = x₁
POL(#pos(x₁)) = 0
POL(#pred(x₁)) = [1]
POL(#s(x₁)) = [1]
POL(#succ(x₁)) = x₁
POL(*(x₁, x₂)) = 0
POL(*'(x₁, x₂)) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(+'(x₁, x₂)) = x₁
POL(::(x₁, x₂)) = [1] + x₂
POL(COMPUTELINE(x₁, x₂, x₃)) = 0
POL(COMPUTELINE#1(x₁, x₂, x₃)) = 0
POL(COMPUTELINE#2(x₁, x₂, x₃, x₄)) = 0
POL(LINEMULT(x₁, x₂, x₃)) = 0
POL(LINEMULT#1(x₁, x₂, x₃)) = 0
POL(LINEMULT#2(x₁, x₂, x₃, x₄)) = 0
POL(MATRIXMULT(x₁, x₂)) = [1] + x₁
POL(MATRIXMULT#1(x₁, x₂)) = x₁
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c27(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(lineMult(x₁, x₂, x₃)) = 0
POL(lineMult#1(x₁, x₂, x₃)) = 0
POL(lineMult#2(x₁, x₂, x₃, x₄)) = 0
POL(nil) = 0

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
+(z0, z1) → #add(z0, z1)
*(z0, z1) → #mult(z0, z1)
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

K tuples:

MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))

Defined Rule Symbols:

lineMult, lineMult#1, lineMult#2, +, *, #mult, #natmult, #add, #succ, #pred

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
+(z0, z1) → #add(z0, z1)
*(z0, z1) → #mult(z0, z1)
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

K tuples:

MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))

Defined Rule Symbols:

lineMult, lineMult#1, lineMult#2, +, *, #mult, #natmult, #add, #succ, #pred

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))

We considered the (Usable) Rules:

#mult(#0, #neg(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#0, #0) → #0
*(z0, z1) → #mult(z0, z1)
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))

And the Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(#0) = 0
POL(#ADD(x₁, x₂)) = x₁
POL(#MULT(x₁, x₂)) = 0
POL(#NATMULT(x₁, x₂)) = 0
POL(#add(x₁, x₂)) = 0
POL(#mult(x₁, x₂)) = 0
POL(#natmult(x₁, x₂)) = 0
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#pred(x₁)) = 0
POL(#s(x₁)) = 0
POL(#succ(x₁)) = 0
POL(*(x₁, x₂)) = 0
POL(*'(x₁, x₂)) = 0
POL(+(x₁, x₂)) = 0
POL(+'(x₁, x₂)) = x₁
POL(::(x₁, x₂)) = [1] + x₁ + x₂
POL(COMPUTELINE(x₁, x₂, x₃)) = x₁
POL(COMPUTELINE#1(x₁, x₂, x₃)) = x₁
POL(COMPUTELINE#2(x₁, x₂, x₃, x₄)) = x₃ + x₄
POL(LINEMULT(x₁, x₂, x₃)) = 0
POL(LINEMULT#1(x₁, x₂, x₃)) = 0
POL(LINEMULT#2(x₁, x₂, x₃, x₄)) = 0
POL(MATRIXMULT(x₁, x₂)) = x₁
POL(MATRIXMULT#1(x₁, x₂)) = x₁
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c27(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(lineMult(x₁, x₂, x₃)) = 0
POL(lineMult#1(x₁, x₂, x₃)) = 0
POL(lineMult#2(x₁, x₂, x₃, x₄)) = 0
POL(nil) = 0

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
+(z0, z1) → #add(z0, z1)
*(z0, z1) → #mult(z0, z1)
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

K tuples:

MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))

Defined Rule Symbols:

lineMult, lineMult#1, lineMult#2, +, *, #mult, #natmult, #add, #succ, #pred

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(17) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
+(z0, z1) → #add(z0, z1)
*(z0, z1) → #mult(z0, z1)
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

K tuples:

MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))

Defined Rule Symbols:

lineMult, lineMult#1, lineMult#2, +, *, #mult, #natmult, #add, #succ, #pred

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(#0) = [2]
POL(#ADD(x₁, x₂)) = 0
POL(#MULT(x₁, x₂)) = x₂
POL(#NATMULT(x₁, x₂)) = 0
POL(#add(x₁, x₂)) = x₁²
POL(#mult(x₁, x₂)) = [2] + x₁ + x₂ + x₁²
POL(#natmult(x₁, x₂)) = 0
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = [1]
POL(#pred(x₁)) = [2] + x₁
POL(#s(x₁)) = 0
POL(#succ(x₁)) = [1]
POL(*(x₁, x₂)) = [2]x₂ + [2]x₁²
POL(*'(x₁, x₂)) = [2]x₂
POL(+(x₁, x₂)) = [1] + x₁ + [2]x₂ + x₂² + x₁²
POL(+'(x₁, x₂)) = 0
POL(::(x₁, x₂)) = [2] + x₁ + x₂
POL(COMPUTELINE(x₁, x₂, x₃)) = x₁ + x₂ + x₁·x₂
POL(COMPUTELINE#1(x₁, x₂, x₃)) = x₃ + x₁·x₃
POL(COMPUTELINE#2(x₁, x₂, x₃, x₄)) = [2]x₁ + x₁·x₄ + x₁·x₃
POL(LINEMULT(x₁, x₂, x₃)) = x₁·x₂
POL(LINEMULT#1(x₁, x₂, x₃)) = x₁·x₃
POL(LINEMULT#2(x₁, x₂, x₃, x₄)) = [2]x₂ + x₂·x₄
POL(MATRIXMULT(x₁, x₂)) = x₁ + x₂ + [2]x₁·x₂
POL(MATRIXMULT#1(x₁, x₂)) = x₁ + x₂ + [2]x₁·x₂
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c27(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(lineMult(x₁, x₂, x₃)) = [2]x₁ + [2]x₁²
POL(lineMult#1(x₁, x₂, x₃)) = [1] + [2]x₁ + x₂ + [2]x₃ + [2]x₂·x₃ + x₁·x₃ + x₁² + x₁·x₂ + x₂²
POL(lineMult#2(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₃·x₄ + x₁·x₄ + [2]x₁·x₂ + x₁·x₃ + x₃² + [2]x₂·x₃ + [2]x₂²
POL(nil) = 0

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
+(z0, z1) → #add(z0, z1)
*(z0, z1) → #mult(z0, z1)
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

K tuples:

MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))

Defined Rule Symbols:

lineMult, lineMult#1, lineMult#2, +, *, #mult, #natmult, #add, #succ, #pred

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(#0) = [1]
POL(#ADD(x₁, x₂)) = 0
POL(#MULT(x₁, x₂)) = x₁·x₂
POL(#NATMULT(x₁, x₂)) = 0
POL(#add(x₁, x₂)) = [1] + x₂ + x₂² + x₁²
POL(#mult(x₁, x₂)) = [2]
POL(#natmult(x₁, x₂)) = [2]x₁·x₂
POL(#neg(x₁)) = [1]
POL(#pos(x₁)) = [1]
POL(#pred(x₁)) = x₁
POL(#s(x₁)) = 0
POL(#succ(x₁)) = 0
POL(*(x₁, x₂)) = 0
POL(*'(x₁, x₂)) = x₁·x₂
POL(+(x₁, x₂)) = [1] + x₁ + x₂ + [2]x₂² + [2]x₁·x₂ + [2]x₁²
POL(+'(x₁, x₂)) = 0
POL(::(x₁, x₂)) = [1] + x₁ + x₂
POL(COMPUTELINE(x₁, x₂, x₃)) = [2]x₁² + [2]x₁·x₂
POL(COMPUTELINE#1(x₁, x₂, x₃)) = [2]x₁·x₃ + [2]x₁²
POL(COMPUTELINE#2(x₁, x₂, x₃, x₄)) = x₃ + x₄ + [2]x₄² + x₃·x₄ + [2]x₁·x₄ + [2]x₁·x₃ + x₃²
POL(LINEMULT(x₁, x₂, x₃)) = x₁ + x₁·x₂
POL(LINEMULT#1(x₁, x₂, x₃)) = x₃ + x₁·x₃
POL(LINEMULT#2(x₁, x₂, x₃, x₄)) = [2]x₂ + x₂·x₄ + x₂·x₃
POL(MATRIXMULT(x₁, x₂)) = [2] + x₂ + [2]x₁·x₂ + [2]x₁²
POL(MATRIXMULT#1(x₁, x₂)) = [2] + [2]x₁·x₂ + [2]x₁²
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c27(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(lineMult(x₁, x₂, x₃)) = x₃² + [2]x₁·x₃
POL(lineMult#1(x₁, x₂, x₃)) = [1] + x₁ + [2]x₂ + [2]x₃ + x₃² + [2]x₂·x₃ + x₁·x₃ + x₁² + x₁·x₂ + x₂²
POL(lineMult#2(x₁, x₂, x₃, x₄)) = [2] + [2]x₁ + x₂ + [2]x₃ + x₄² + x₃·x₄ + x₂·x₄ + [2]x₁·x₄ + [2]x₁² + [2]x₁·x₂ + x₁·x₃ + [2]x₃² + x₂·x₃ + [2]x₂²
POL(nil) = 0

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
+(z0, z1) → #add(z0, z1)
*(z0, z1) → #mult(z0, z1)
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

K tuples:

MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))

Defined Rule Symbols:

lineMult, lineMult#1, lineMult#2, +, *, #mult, #natmult, #add, #succ, #pred

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(#0) = 0
POL(#ADD(x₁, x₂)) = 0
POL(#MULT(x₁, x₂)) = 0
POL(#NATMULT(x₁, x₂)) = 0
POL(#add(x₁, x₂)) = [2] + x₁ + [2]x₂² + x₁²
POL(#mult(x₁, x₂)) = [2] + x₁ + x₂ + [2]x₁·x₂
POL(#natmult(x₁, x₂)) = [1] + [2]x₁·x₂ + x₁²
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#pred(x₁)) = [2] + x₁ + x₁²
POL(#s(x₁)) = [2]
POL(#succ(x₁)) = [2]
POL(*(x₁, x₂)) = x₁ + [2]x₁²
POL(*'(x₁, x₂)) = 0
POL(+(x₁, x₂)) = [1] + [2]x₁ + [2]x₁·x₂ + [2]x₁²
POL(+'(x₁, x₂)) = 0
POL(::(x₁, x₂)) = [1] + x₁ + x₂
POL(COMPUTELINE(x₁, x₂, x₃)) = x₂
POL(COMPUTELINE#1(x₁, x₂, x₃)) = x₃
POL(COMPUTELINE#2(x₁, x₂, x₃, x₄)) = x₁
POL(LINEMULT(x₁, x₂, x₃)) = x₂
POL(LINEMULT#1(x₁, x₂, x₃)) = x₁
POL(LINEMULT#2(x₁, x₂, x₃, x₄)) = x₄
POL(MATRIXMULT(x₁, x₂)) = [2] + x₁ + x₁·x₂ + x₁²
POL(MATRIXMULT#1(x₁, x₂)) = [1] + x₁·x₂ + x₁²
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c27(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(lineMult(x₁, x₂, x₃)) = [2]x₁ + [2]x₂·x₃ + x₁·x₃ + x₁² + x₁·x₂
POL(lineMult#1(x₁, x₂, x₃)) = [1] + [2]x₁ + [2]x₂ + [2]x₃ + x₃² + [2]x₂·x₃ + x₁·x₃ + x₁² + [2]x₁·x₂ + [2]x₂²
POL(lineMult#2(x₁, x₂, x₃, x₄)) = x₁ + [2]x₂ + [2]x₃ + x₄ + [2]x₄² + x₃·x₄ + x₂·x₄ + x₁·x₂ + x₁·x₃ + [2]x₃² + x₂²
POL(nil) = 0

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
+(z0, z1) → #add(z0, z1)
*(z0, z1) → #mult(z0, z1)
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

K tuples:

MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))

Defined Rule Symbols:

lineMult, lineMult#1, lineMult#2, +, *, #mult, #natmult, #add, #succ, #pred

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(25) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
+'(z0, z1) → c1(#ADD(z0, z1))
*'(z0, z1) → c(#MULT(z0, z1))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
*'(z0, z1) → c(#MULT(z0, z1))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
+(z0, z1) → #add(z0, z1)
*(z0, z1) → #mult(z0, z1)
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:

#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

K tuples:

MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
+'(z0, z1) → c1(#ADD(z0, z1))
*'(z0, z1) → c(#MULT(z0, z1))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))

Defined Rule Symbols:

lineMult, lineMult#1, lineMult#2, +, *, #mult, #natmult, #add, #succ, #pred

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(27) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(#0) = 0
POL(#ADD(x₁, x₂)) = 0
POL(#MULT(x₁, x₂)) = x₁
POL(#NATMULT(x₁, x₂)) = x₁
POL(#add(x₁, x₂)) = 0
POL(#mult(x₁, x₂)) = [2] + [2]x₁²
POL(#natmult(x₁, x₂)) = [2]x₂²
POL(#neg(x₁)) = x₁
POL(#pos(x₁)) = x₁
POL(#pred(x₁)) = [2] + x₁²
POL(#s(x₁)) = [2] + x₁
POL(#succ(x₁)) = [1]
POL(*(x₁, x₂)) = [2]
POL(*'(x₁, x₂)) = x₁
POL(+(x₁, x₂)) = [1] + x₁ + [2]x₂ + x₁·x₂ + [2]x₁²
POL(+'(x₁, x₂)) = 0
POL(::(x₁, x₂)) = [1] + x₁ + x₂
POL(COMPUTELINE(x₁, x₂, x₃)) = x₂
POL(COMPUTELINE#1(x₁, x₂, x₃)) = x₃
POL(COMPUTELINE#2(x₁, x₂, x₃, x₄)) = x₁
POL(LINEMULT(x₁, x₂, x₃)) = x₂
POL(LINEMULT#1(x₁, x₂, x₃)) = x₁
POL(LINEMULT#2(x₁, x₂, x₃, x₄)) = x₃ + x₄
POL(MATRIXMULT(x₁, x₂)) = [2]x₁·x₂
POL(MATRIXMULT#1(x₁, x₂)) = [2]x₁·x₂
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c27(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(lineMult(x₁, x₂, x₃)) = [2]x₂ + [2]x₁² + [2]x₂²
POL(lineMult#1(x₁, x₂, x₃)) = [2] + x₁ + x₂ + [2]x₃ + x₂·x₃ + [2]x₁·x₃ + x₁² + x₁·x₂ + x₂²
POL(lineMult#2(x₁, x₂, x₃, x₄)) = [2]x₁ + x₃ + x₃·x₄ + [2]x₁·x₄ + x₃² + [2]x₂²
POL(nil) = 0

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
+(z0, z1) → #add(z0, z1)
*(z0, z1) → #mult(z0, z1)
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:

#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

K tuples:

MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
+'(z0, z1) → c1(#ADD(z0, z1))
*'(z0, z1) → c(#MULT(z0, z1))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))

Defined Rule Symbols:

lineMult, lineMult#1, lineMult#2, +, *, #mult, #natmult, #add, #succ, #pred

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(29) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

We considered the (Usable) Rules:

#succ(#0) → #pos(#s(#0))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#succ(#neg(#s(#0))) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#mult(#0, #neg(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#0, #0) → #0
*(z0, z1) → #mult(z0, z1)
#natmult(#0, z0) → #0
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))

And the Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(#0) = 0
POL(#ADD(x₁, x₂)) = x₁
POL(#MULT(x₁, x₂)) = x₁·x₂
POL(#NATMULT(x₁, x₂)) = x₁·x₂
POL(#add(x₁, x₂)) = x₁ + x₂
POL(#mult(x₁, x₂)) = x₁·x₂
POL(#natmult(x₁, x₂)) = x₁·x₂
POL(#neg(x₁)) = x₁
POL(#pos(x₁)) = x₁
POL(#pred(x₁)) = [2]
POL(#s(x₁)) = [1] + x₁
POL(#succ(x₁)) = [1] + x₁
POL(*(x₁, x₂)) = x₁·x₂
POL(*'(x₁, x₂)) = x₁·x₂
POL(+(x₁, x₂)) = [2] + [2]x₂ + [2]x₂² + x₁·x₂
POL(+'(x₁, x₂)) = x₁
POL(::(x₁, x₂)) = [2] + x₁ + x₂
POL(COMPUTELINE(x₁, x₂, x₃)) = [2]x₁ + [2]x₁·x₂
POL(COMPUTELINE#1(x₁, x₂, x₃)) = [2]x₁·x₃
POL(COMPUTELINE#2(x₁, x₂, x₃, x₄)) = [2]x₁ + [2]x₁·x₄ + [2]x₁·x₃
POL(LINEMULT(x₁, x₂, x₃)) = [1] + [2]x₁·x₂
POL(LINEMULT#1(x₁, x₂, x₃)) = [1] + [2]x₁·x₃
POL(LINEMULT#2(x₁, x₂, x₃, x₄)) = [1] + [2]x₂·x₄ + [2]x₂·x₃
POL(MATRIXMULT(x₁, x₂)) = [2]x₁ + x₂ + [2]x₁·x₂
POL(MATRIXMULT#1(x₁, x₂)) = [2]x₁ + x₂ + [2]x₁·x₂
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c19(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c24(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c27(x₁)) = x₁
POL(c28(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c30(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(lineMult(x₁, x₂, x₃)) = [1] + x₂ + x₃² + [2]x₁·x₃ + [2]x₁²
POL(lineMult#1(x₁, x₂, x₃)) = [2] + [2]x₁ + x₃ + x₃² + x₁·x₃ + [2]x₁² + [2]x₁·x₂ + x₂²
POL(lineMult#2(x₁, x₂, x₃, x₄)) = [2] + [2]x₁ + [2]x₂ + x₃ + x₄² + [2]x₃·x₄ + x₂·x₄ + [2]x₁·x₄ + [2]x₁·x₂ + [2]x₃² + x₂·x₃ + x₂²
POL(nil) = 0

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0)
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1)
lineMult#1(nil, z0, z1) → nil
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1))
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil))
+(z0, z1) → #add(z0, z1)
*(z0, z1) → #mult(z0, z1)
#mult(#0, #0) → #0
#mult(#0, #neg(z0)) → #0
#mult(#0, #pos(z0)) → #0
#mult(#neg(z0), #0) → #0
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) → #0
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1))
#natmult(#0, z0) → #0
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1))
#add(#pos(#s(#0)), z0) → #succ(z0)
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1))
#add(#0, z0) → z0
#add(#neg(#s(#0)), z0) → #pred(z0)
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0))
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(z0))) → #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

Tuples:

*'(z0, z1) → c(#MULT(z0, z1))
+'(z0, z1) → c1(#ADD(z0, z1))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

S tuples:none
K tuples:

MATRIXMULT(z0, z1) → c12(MATRIXMULT#1(z0, z1))
#ADD(#neg(#s(#s(z0))), z1) → c17(#ADD(#pos(#s(z0)), z1))
MATRIXMULT#1(::(z0, z1), z2) → c13(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))
COMPUTELINE#1(::(z0, z1), z2, z3) → c3(COMPUTELINE#2(z3, z2, z0, z1))
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c5(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))
COMPUTELINE(z0, z1, z2) → c2(COMPUTELINE#1(z0, z2, z1))
#MULT(#neg(z0), #pos(z1)) → c25(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) → c28(#NATMULT(z0, z1))
#MULT(#neg(z0), #neg(z1)) → c24(#NATMULT(z0, z1))
#MULT(#pos(z0), #neg(z1)) → c27(#NATMULT(z0, z1))
LINEMULT#1(::(z0, z1), z2, z3) → c8(LINEMULT#2(z2, z3, z0, z1))
LINEMULT#2(::(z0, z1), z2, z3, z4) → c10(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1))
LINEMULT#2(nil, z0, z1, z2) → c11(*'(z1, z0), LINEMULT(z0, z2, nil))
+'(z0, z1) → c1(#ADD(z0, z1))
*'(z0, z1) → c(#MULT(z0, z1))
LINEMULT(z0, z1, z2) → c7(LINEMULT#1(z1, z2, z0))
#NATMULT(#s(z0), z1) → c30(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#ADD(#pos(#s(#s(z0))), z1) → c19(#ADD(#pos(#s(z0)), z1))

Defined Rule Symbols:

lineMult, lineMult#1, lineMult#2, +, *, #mult, #natmult, #add, #succ, #pred

Defined Pair Symbols:

*', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #MULT, #NATMULT, #ADD

Compound Symbols:

c, c1, c2, c3, c5, c7, c8, c10, c11, c12, c13, c24, c25, c27, c28, c30, c17, c19

(31) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(0) Obligation:

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

(2) Obligation:

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) CdtUsableRulesProof (EQUIVALENT transformation)

(10) Obligation:

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(12) Obligation:

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(16) Obligation:

(17) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(20) Obligation:

(21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(22) Obligation:

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(24) Obligation:

(25) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(26) Obligation:

(27) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(28) Obligation:

(29) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(30) Obligation:

(31) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

(32) BOUNDS(1, 1)